29874d2a88a6b203cce9618a8cb6824611b5c711,jayhorn/src/main/java/jayhorn/hornify/encoder/MethodEncoder.java,MethodEncoder,encodeEmptyMethod,#,75
Before Change
final Map<Variable, ProverExpr> varMap = new HashMap<Variable, ProverExpr>();
final ProverExpr entryAtom = precondition.instPredicate(varMap);
final ProverExpr exitAtom = postcondition.instPredicate(varMap);
clauses.add(p.mkHornClause(exitAtom, new ProverExpr[] { entryAtom }, p.mkLiteral(true)));
}
/**
After Change
final Map<Variable, ProverExpr> varMap = new HashMap<Variable, ProverExpr>();
final ProverExpr entryAtom = precondition.instPredicate(varMap);
final ProverExpr exitAtom = postcondition.instPredicate(varMap);
final ProverHornClause clause = p.mkHornClause(exitAtom, new ProverExpr[] { entryAtom }, p.mkLiteral(true));
tsClauses.add(clause);
S2H.sh().addClause((Statement)null, tsClauses);
clauses.add(clause);
}
/**